$\forall$$A$, $B$:Type, $c$:$\mathbb{B}$, $f$:($A$$\rightarrow$$B$), $x$, $y$:$A$. $f$(if $c$$\rightarrow$ $x$ else $y$ fi) $=$ if $c$$\rightarrow$ $f$($x$) else $f$($y$) fi